Inference at * 1 
Iof proof for Lemma lt int eq false elim sqequal:



1. i : 
2. j : 
  (i <z j ~ ff)  ((i < j)) 

latex

 by D 0 

latex

 1: 

 1: 3. i <z j ~ ff
 1:   (i < j)
 2: .....wf..... NILNIL

 2:   (i <z j ~ ff)  Type
 .

Definitions	P  Q, t  T
Lemmas	not wf